% Copyright Kani Contributors
% SPDX-License-Identifier: Apache-2.0 OR MIT

\begin{paper}{8}
@inproceedings{verus-sys,
  author    = {Lattuada, Andrea and Hance, Travis and Bosamiya, Jay and Brun, Matthias and Cho, Chanhee and LeBlanc, Hayley and Srinivasan, Pranav and Achermann, Reto and Chajed, Tej and Hawblitzel, Chris and Howell, Jon and Lorch, Jay and Padon, Oded and Parno, Bryan},
  booktitle = {Proceedings of the ACM Symposium on Operating Systems Principles (SOSP)},
  code      = {https://github.com/verus-lang/verus},
  month     = {November},
  title     = {Verus: A Practical Foundation for Systems Verification},
  year      = {2024}
}

@inproceedings{denis2022creusot, 
  title={Creusot: a foundry for the deductive verification of {R}ust programs}, 
  author={Denis, Xavier and Jourdan, Jacques-Henri and March{'e}, Claude}, 
  booktitle={International Conference on Formal Engineering Methods}, 
  pages={90--105}, 
  year={2022}, 
  organization={Springer} 
}

@inproceedings{astrauskas2022prusti,
  title={The {P}rusti project: Formal verification for {R}ust},
  author={Astrauskas, Vytautas and B{\'\i}l{\`y}, Aurel and Fiala, Jon{\'a}{\v{s}} and Grannan, Zachary and Matheja, Christoph and M{\"u}ller, Peter and Poli, Federico and Summers, Alexander J},
  booktitle={NASA Formal Methods Symposium},
  pages={88--108},
  year={2022},
  organization={Springer}
}

@inproceedings{vanhattum2022verifying,
  title={Verifying dynamic trait objects in {R}ust},
  author={VanHattum, Alexa and Schwartz-Narbonne, Daniel and Chong, Nathan and Sampson, Adrian},
  booktitle={Proceedings of the 44th International Conference on Software Engineering: Software Engineering in Practice},
  pages={321--330},
  year={2022}
}

@manual{superPower,
    title = {Unsafe Rust},
    url = {https://doc.rust-lang.org/book/ch19-01-unsafe-rust.html},
    author = {Rust Documentation}
}

@inproceedings{li2021mirchecker,
  title={MirChecker: detecting bugs in {R}ust programs via static analysis},
  author={Li, Zhuohua and Wang, Jincheng and Sun, Mingshen and Lui, John CS},
  booktitle={Proceedings of the 2021 ACM SIGSAC conference on computer and communications security},
  pages={2183--2196},
  year={2021}
}

@manual{stringChallenge,
    title = {Memory Safety of String},
    year = {2024},
    author = {Zyad Hassan},
    url = {https://model-checking.github.io/verify-rust-std/challenges/0010-string.html}
}

@manual{anderson20medium,
    title = {The Rust Compilation Model Calamity}, 
    year = {2020},
    url = {https://pingcap.medium.com/the-rust-compilation-model-calamity-1a8ce781cf6cb},
    author = {Brian Anderson}
}

@article{matsakis2014rust,
  title={The rust language},
  author={Matsakis, Nicholas D and Klock, Felix S},
  journal={ACM SIGAda Ada Letters},
  volume={34},
  number={3},
  pages={103--104},
  year={2014},
  publisher={ACM New York, NY, USA}
}

@manual{challenge,
    title = {Memory Safety of String},
    url = {https://github.com/model-checking/verify-rust-std/issues/61},
    author = {Zyad Hassan},
    year = {2024}
}

@manual{solution,
  title = {char and ascii{\_}char contracts},
  url = {https://github.com/model-checking/verify-rust-std/pull/48},
  year = {2024},
  author = {Carolyn Zech}
}

@manual{rustAndroid,
  title = {The Impact of Rust on Security Development},
  year = {2024},
  url = {https://www.riscure.com/the-impact-of-rust-on-security-development},
  author = {Christiaan Biesterbosch and Valeria Vatolina}
}
@manual{liam2022android,
    title = {How Google is using Rust to reduce memory safety vulnerabilities in Android},
    year = {2020},
    url = {https://www.zdnet.com/article/google-after-using-rust-we-slashed-android-memory-safety-vulnerabilities/},
    author = {Liam Tung}
}

@article{jung2017rustbelt,
  title={RustBelt: Securing the foundations of the Rust programming language},
  author={Jung, Ralf and Jourdan, Jacques-Henri and Krebbers, Robbert and Dreyer, Derek},
  journal={Proceedings of the ACM on Programming Languages},
  volume={2},
  number={POPL},
  pages={1--34},
  year={2017},
  publisher={ACM New York, NY, USA}
}

@article{ayoun2024hybrid,
  title={A hybrid approach to semi-automated Rust verification},
  author={Ayoun, Sacha-{\'E}lie and Denis, Xavier and Maksimovi{\'c}, Petar and Gardner, Philippa},
  journal={arXiv preprint arXiv:2403.15122},
  year={2024}
}

@article{ho2022aeneas,
  title={Aeneas: Rust verification by functional translation},
  author={Ho, Son and Protzenko, Jonathan},
  journal={Proceedings of the ACM on Programming Languages},
  volume={6},
  number={ICFP},
  pages={711--741},
  year={2022},
  publisher={ACM New York, NY, USA}
}

\end{thebibliography}